es:ES, A:Type, l:IdLnk, tg:Id, ds:x:Id fp Type,
conds:k:Knd fp V:Type  (State(ds)V(A + Top)).
(k:Knd. (k  dom(conds))  (hasloc(k;source(l))))
 (e:E. (kind(e) = rcv(l,tg)  Knd)  (valtype(e) r A))
 (p:(e:E.
 (p:(Dec((isrcv(e))
 (p:(& lnk(e) = l
 (p:(& loc(sender(e)) = source(l)  Id
 (p:(& (kind(sender(e))  dom(conds)))).
 (k:Knd.
 (k  dom(conds))
  k(v:conds(k).1) sends on l [tg:A, p.let s,v = p in (conds(k).2)(s,v) <state, v>]?[])
  glues(es;
  glues(A;
  glues((e.sender(e));
  glues((e.outl((conds(kind(e)).2)((state when e),val(e))));
  glues(es-triggers(es;source(l);ds;conds);
  glues((es-in-port(es;l;tg)|p))) 

latex

Definitions

ES, t  T, f(a), EState(T), Id, , x:AB(x), x:A. B(x), pred!(e;e'), SWellFounded(R(x;y)), Unit, Void, x:A.B(x), Top, S  T, left + right, Type, suptype(S; T), first(e), b, A, loc(e), <a, b>, s = t, P  Q, constant_function(f;A;B), IdLnk, x,y. t(x;y), x. t(x), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, x:A  B(x), P & Q, , r  s, e < e', val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), , Msg(M), type List, kind(e), EOrderAxioms(E; pred?; info), EqDecider(T), (x  l), {x:A| B(x)} , Atom$n, State(ds), a:A fp B(a), x.A(x), source(l), hasloc(k;i), KindDeq, x  dom(f), valtype(e), rcv(l,tg), kind(e), E, if b then t else f fi , sender(e), loc(e), lnk(e), t.1, ff, tt, locl(a), let x,y = A in B(x;y), False, True, case b of inl(x) => s(x) | inr(y) => t(y), , A c B, Dec(P), isrcv(e), f(x), t.2, k(v:B) sends on l [tg:T, f <state, v>]?[], es-triggers(es;i;ds;conds), glues(es; B; g; f; Ia; Ib), a = b, P  Q, P  Q, {T}, state@i, IdDeq, f(x)?z, vartype(i;x)

Lemmas

es-state-subtype-iff, es-state-subtype, es-vartype wf, fpf-cap wf, id-deq wf, sender-glues-triggers, all functionality wrt iff, implies functionality wrt iff, assert-eq-knd, eq knd wf, subtype rel wf, conditional-send-p wf, pi2 wf, pi1 wf, fpf-ap wf, es-isrcv wf, decidable wf, true wf, false wf, locl wf, btrue wf, bfalse wf, es-lnk wf, es-loc wf, es-sender wf, es-E wf, es-kind wf, rcv wf, es-valtype wf, fpf-dom wf, Kind-deq wf, hasloc wf, lsrc wf, fpf-trivial-subtype-top, decl-state wf, l member wf, deq wf, EOrderAxioms wf, Id wf, kind wf, loc wf, Msg wf, nat wf, val-axiom wf, cless wf, qle wf, bool wf, rationals wf, Knd wf, kindcase wf, IdLnk wf, EState wf, constant function wf, not wf, assert wf, first wf, top wf, unit wf, event system wf